@$i$ stable ${\it state}$.$P$(${\it state}$)   $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$e$@$i$. $P$((state when $e$)) $\Rightarrow$ $P$(state after $e$)